A, B, C:Realizer. A  B  B  C  A  C 

latex

Definitions	x:A. B(x), P  Q, A  B, t  T, Prop, Y, if b t else f fi, True, P & Q, true, false, SQType(T), {T}, AB, A, False, ij, P  Q, , , Unit, P  Q, , b, Rplus?(x1),
Lemmas	nat wf, R-size wf, nat plus wf, R-sub wf, es realizer wf, le wf, Rnone? wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, bool cases, bool sq, Rplus? wf, R-size-decreases, Rplus-left wf, Rplus-right wf, nat properties, ge wf, Rnone?-implies